/*@ n>0
 */
int sum (int n)
{
  int s;
  if (n==0)
    return 0;
  else {
    s = sum(n-1);
    s = s + n;
    return s;
  }
}
/*@ 2*result == n*(n+1)
 */


